{-bKung f as  = bs
	where
	(ls,rs) = splitAt ((length as)`div`2) as
	(out1,out2) = (bKung f ls, bKung f rs)
	outs = f[last out1 ,last out2]
	bs = out1 ++ (init out2) ++ [last outs]-}
{---A6
addOp :: Fan (Signal Int)
addOp [] = []
addOp [a] = [a]
addOp [a,b] = [a+b]

delayOp :: Fan (Signal Int)
delayOp as = [(1 + maximum as)]

carryOp :: Fan (Bit,Bit)
carryOp [(g',p'),(g,p)] = [(a,b)]
	where
	 a = (g<|>(p<&>g'))
	 b = (p<&>p')

listLast [] = []
listLast a = last a

mapNxN :: Int -> PP a
mapNxN n f [] = []
mapNxN n f [a] = [a]
mapNxN n f as = l ++ newR ++ val ++ ((mapNxN n f) next)
	where
	(this,next) = splitAt n as
	(l,r) = splitAt (length this `div` 2) this
	val = f([last l] ++ [last r])
	(newR,drop) = splitAt ((length r) - 1) r

invMapNxN :: Int -> PP a
invMapNxN n f [] = []
invMapNxN n f as =  ls ++ newLR ++ val ++ rrs ++ ((invMapNxN n f) newNext)
	where
	(this,next) = splitAt n as
	(ls,rs) = splitAt (length this `div` 2) this
	(lrs,rrs) = splitAt (length rs `div` 2) rs
	
	val = f([last ls] ++ [last lrs])
	(newLR,drop) = splitAt ((length lrs) - 1) lrs
	
	(nextL,nextR) = splitAt (length lrs) next
	nextVal =  if null nextL then [] else f([last this] ++ [last nextL])
	(newNextL,nxtdrop) = if null nextL then ([],[]) else splitAt ((length nextL) - 1) nextL
	(newNext) = (newNextL ++ nextVal ++ nextR)

topTree :: Int -> PP a

topTree n f as = aOuts
	where
	aNext = (mapNxN n f) as
	aOuts = if n == length as
			then aNext
			else (topTree (n*2) f) aNext

invTree n f as = aOuts
	where
	aNext = (invMapNxN n f) as
	aOuts = if n == 8
			then aNext
			else (invTree (n`div`2) f) aNext

bKung :: PP a
bKung f [a] = [a]
bKung f as  = b0:bs
	where
	--xs = ((mapNxN 64 f)((mapNxN 32 f)((mapNxN 16 f)((mapNxN 8 f)((mapNxN 4 f)((mapNxN 2 f) as))))))
	--ys = ((invMapNxN 8 f)((invMapNxN 16 f)((invMapNxN 32 f)((invMapNxN 64 f) xs))))
	xs = (topTree 2 f) as	
	ys = (invTree (length as) f) xs
	b0 = head ys
	bs = (mapNxN 2 f) (tail ys)

gpGen :: [(Bit,Bit)] -> [(Bit,Bit)]
gpGen [] = []
gpGen ((a1,b1):gps) = [(g1,p1)] ++ gpGen(gps)
	where
	(g1,p1) = gpC(a1,b1)

finalSum :: (Bit,[(Bit,Bit)]) -> [Bit]
finalSum (gn,[]) = [gn]
finalSum (cin,(g1,p1):gps) = [s1] ++ sOut
	where
	s1 = sumC(cin,(g1,p1))
	sOut = finalSum(g1,gps)

fastAdderBK :: [(Bit, Bit)] -> [Bit]
fastAdderBK abs = ss
  where
  inGps = gpGen abs
  outGps = ((bKung carryOp) inGps)
  (initialGs,initialPs) = unzipp(inGps)
  (finalGs,finalPs) = unzipp(outGps)
  ss = finalSum (low,zipp(finalGs,initialPs))


-- exhaustive test  
inpGen n a b = outBin
	where
	x = int2bin n a
	y = int2bin n b
	outBin = (simulate zipp)(x,y)

testfastAdderBK n a b = simulate equal (bkOut,intOut)
	where
	bkOut = (simulate bin2int) (simulate fastAdderBK (inpGen n a b))
	intOut = simulate plus (a,b)

exhaustiveTester l n = ([ testfastAdderBK l x y | x<-[0..m],y<-[0..m]])
	where
	m = fromInteger (2^n-1)

testA6x0 = exhaustiveTester 8 2
testA6x1 = exhaustiveTester 8 4
testA6x2 = exhaustiveTester 16 2
testA6x3 = exhaustiveTester 16 4

exhaustiveTestBKfastAdder = do
							testA6x0
							testA6x1
							testA6x2
							testA6x3

--formal verification
bKungOPEqualityChecker :: (Binary,(Binary,Bit)) -> Bit
bKungOPEqualityChecker (as,(bs,b)) = (as<==>(bs ++ [b]))

propBKOPEquivalenceCheck a = ok
	where
	out1 = fastAdderBK a
	out2 = adder6 a
	ok = bKungOPEqualityChecker(out1,out2)

propBKOPEquivalenceCheckForSizeN n = forAll (list n) $ \as -> propBKOPEquivalenceCheck as

testA6x4 = smv (propBKOPEquivalenceCheckForSizeN 8)
testA6x5 = smv (propBKOPEquivalenceCheckForSizeN 16)

formalVerificationBKfastAdder = do
								testA6x4
								testA6x5
-- depth bKung

depthTestBkung n = simulate (bKung delayOp) (replicate n 0)

testA6x6 = depthTestBkung 8
testA6x7 = depthTestBkung 16
testA6x8 = depthTestBkung 32

depthTestBKPrefixNet = do
					   testA6x6
					   testA6x7
					   testA6x8

--A7
opCount :: Fan (Signal Int)
opCount as = [(1 + minimum as)]

addList :: [Signal Int] -> Signal Int
addList [a] = a
addList (a:b:cs) = addList((a+b):cs)

opCountTestBkung n = simulate (bKung opCount) (replicate n 0)

testA7x0 = simulate addList (opCountTestBkung 8)
testA7x1 = simulate addList (opCountTestBkung 16)

--A8
-- i starts from 1
oneArmFan :: Int -> Int -> PP a
oneArmFan i span f as = cs
	where
	--(elems) = [m*(length as)`div`n | m <-[0..n-1]]
	firstElem = (i)*(length as)`div`span
	secondElem = (i+1)*(length as)`div`span
	newVal = f([as!!(firstElem-1)] ++ [as!!(secondElem-1)])
	(las,ras) = splitAt (secondElem-1) as
	bs = las ++ newVal ++ tail(ras)
	cs = if (i+1) == span
		 then bs
		 else oneArmFan (i+1) span f bs

serialPrefixRow :: Int -> Int -> PP a
serialPrefixRow span chunk f [] = []
serialPrefixRow span chunk f as = bs
	where
	(ls,rs) = splitAt chunk as
	newLs = (oneArmFan 1 span f ls)
	bs = if length rs >= chunk
		 then newLs ++ (serialPrefixRow span chunk f rs)
		 else newLs ++ rs

serialPrefixtree :: Int -> Int -> PP a
serialPrefixtree span chunk f as = aOuts
	where
	bs = serialPrefixRow span chunk f as
	newChunk = (chunk*span)
	aOuts = if (newChunk) > length as
			then bs
			else (serialPrefixtree span newChunk f bs)

manyArmFan :: Int -> Int -> Int -> PP a
manyArmFan i span chunk f [] = []
manyArmFan i span chunk f as = cs
	where
	firstElem = 1-- *(length as)`div`span
	secondElem =firstElem + (i*chunk`div`span)
	newVal = f([as!!(firstElem-1)] ++ [as!!(secondElem-1)])
	(las,ras) = splitAt (secondElem-1) as
	bs = las ++ newVal ++ tail(ras)
	cs = if (i+1) == span || (1+((i+1)*chunk`div`span)) > length bs
		 then bs
		 else manyArmFan (i+1) span chunk f bs

fanRow :: Int -> Int -> Int -> PP a
fanRow i span chunk f [] = []
fanRow i span chunk f as = bs --ls ++ newRs -- (fanRow span chunk f ls) ++ newRs
	where
	(ls,rs) = splitAt ((chunk*i)-1) as
	newRs = (manyArmFan 1 span chunk f rs)
	bs = if (chunk*(i+1)) >= length as
		 then ls ++ newRs
		 else (fanRow (i+1) span chunk) f (ls ++ newRs)
	
	
bKungG :: Int -> PP a
bKungG block f [a] = [a]
bKungG block f as  = zs
	where
	xs = serialPrefixtree block block f as
	ys = fanRow 1 block (block*block) f xs
	zs = fanRow 1 block block f ys
-- span**2 and then span are the chunk length for fan tree	

{-mkFanDiag :: ([a] -> [a]) -> Fan a
--mkFanDiag f [a,al] = a:f[a,al]
mkFanDiag f as = als ++ f[head as,last]
	where
	(als,[last]) = splitAt (length as -1)as

diagPlus :: Fan (Signal Int)
diagPlus [a,b] = [plus(a,b)]

mapN :: Int -> PP a
mapN n f [] = []
mapN n f as = bs
	where
	(ls,rs) = splitAt n as
	newLs = f (ls)
	bs = newLs ++ (mapN n f) rs

bKung :: PP a
bKung f [a] = [a]
bKung f as  = xs
	where
	xs = (mapN 2 f) as-}-}
	
{-
prefixAdder :: Fan (Signal Int)
prefixAdder [a,b] = [a,a+b]
prefixAdder [a,b,c,d] = [a,b,c,b+d]
prefixAdder [a1,a2,a3,a4,a5,a6,a7,a8] = [a1,a2,a3,a4,a5,a6+a4,a7,a8+a4]

gpCalc :: [(Bit,Bit)] -> (Bit,Bit)
gpCalc [(g',p'),(g,p)] = ((g'<|>(p'<&>g)),(p'<&>p))
--gpCalc [a,b,c,d] = gpCalc [gpCalc[a,b],gpCalc[c,d]]

addOp :: Fan (Signal Int)
addOp [a,b] = [a+b]

delayOp :: Fan (Signal Int)
delayOp as = [(1 + maximum as)]


carryOp :: Fan (Bit,Bit)
carryOp [a,b] = [a,gpCalc[a,b]]
carryOp [a,b,c,d] = [a,b,c,gpCalc[b,d]]
carryOp [a1,a2,a3,a4,a5,a6,a7,a8] = [a1,a2,a3,a4,a5,gpCalc[a6,a4],a7,gpCalc[a8,a4]]

map2x2 :: PP a
map2x2 f [] = []
map2x2 f [a] = [a]
--map2x2 f (a:b:cs) = f[a,b] ++ ((map2x2 f) cs)
map2x2 f (a:b:cs) = [a] ++ f[a,b] ++ ((map2x2 f) cs)

map4x4 :: PP a
map4x4 f [] = []
--map4x4 f (a:b:c:d:es) = f[a,b,c,d] ++ ((map4x4 f) es)
map4x4 f (a:b:c:d:es) = [a,b,c] ++ f[b,d] ++ ((map4x4 f) es)

map8x8 :: PP a
map8x8 f [] = []
map8x8 f [a1,a2,a3,a4] = [a1,a2,a3,a4]
--map8x8 f (a1:a2:a3:a4:a5:a6:a7:a8:ai) = f[a1,a2,a3,a4,a5,a6,a7,a8] ++ ((map8x8 f) ai)
map8x8 f (a1:a2:a3:a4:a5:a6:a7:a8:ai) = [a1,a2,a3,a4,a5] ++ f[a4,a6]++ [a7] ++ f[a4,a8] ++ ((map8x8 f) ai)

bKung :: PP a
bKung f [a] = [a]
bKung f as  = e0:es
	where
	bs = (map2x2 f) as
	cs = (map4x4 f) bs
	ds = (map8x8 f) cs
	e0 = head ds
	es = (map2x2 f) (tail ds)-}

--Brent-Kung alternate
{-carryOp :: [(Bit,Bit)] -> (Bit,Bit)
carryOp [(g',p'),(g,p)] = ((g'<|>(p'<&>g)),(p'<&>p))
carryOp [a,b,c,d] = carryOp [carryOp[a,b],carryOp[c,d]]

addOp :: [Signal Int] -> Signal Int
addOp [a,b] = (a+b)
addOp [a,b,c,d] = (a+b+c+d)

fourLineElement f [a,b,c,d] = [a,f[a,b],c,f[a,b,c,d]]
fourLineElement2 f [a,b,c] = [a,f[a,b],c]
fourLineElement2 f [a,b,c,d] = [a,f[a,b],c,f[c,d]]
map4x4 f [] = []
map4x4 f (a1:a2:a3:[]) = f [a1,a2,a3]
map4x4 f (a1:a2:a3:a4:ai) = f[a1,a2,a3,a4] ++ ((map4x4 f) ai)

fanFourthOutput :: ([a]-> a) -> [a] -> [a]
fanFourthOutput f [] = []
fanFourthOutput f [a1,a2,a3,a4] = [a1,a2,a3,a4]
fanFourthOutput f (a1:a2:a3:a4:a5:a6:a7:a8:ai) = [a1,a2,a3,a4] ++ ((fanFourthOutput f) nextAi)
	where
	nextAi = [a5,f[a4,a6],a7,f[a4,a8]] ++ ai

--brentKung :: PP a	
brentKung f as = c0:ds
	where
	bs = (map4x4 (fourLineElement f)) as
	cs = (fanFourthOutput f) bs
	c0 = (head cs)
	ds = (map4x4 (fourLineElement2 f)) (tail cs)-}
{-
pairUpList :: Binary -> [(Bit,Bit)]
pairUpList [] = []
pairUpList [a] = [(a,low)]
pairUpList (a:b:cs) = [(a,b)] ++ (pairUpList cs)-}
{-serialPrefixNetwork :: Int -> PP a
serialPrefixNetwork block f as = outs
	where
	(ls,rs) = splitAt (length as - block) as
	serRes = serialPrefixFan block f rs
	outs = if (ifRoot (length as) block) == 0
		   then serialPrefixFan block f (ls ++ serRes)
		   else ls ++ serRes

serialPrefixNetworkTree :: Int -> Int -> PP a
serialPrefixNetworkTree k block f [] = []
serialPrefixNetworkTree k block f as = result
	where
	(ls,rs) = splitAt block as
	outs = serialPrefixNetwork k f ls
	result = if null rs
			 then outs
			 else serialPrefixNetworkTree k (block+k) f (outs ++ rs)-}
	

{-putInList :: [b] -> PP a
putInList [] as = as
putInList ((e,ind):els) as = out
	where
	(ls,rs) = splitAt (ind+1) as
	out = putInList els ((init ls) ++ e ++ rs)

serialPrefixNetwork :: Int -> PP a
serialPrefixNetwork block f as = outs
	where
	elts = [i*(length as `div` block) | i<-[1..block]]
	ops = [as!!(ind-1) | ind <- elts]
	results = ser f [ops]
	outs = putInList zipp(results,elts) as

serialPrefixNetworkRow :: Int -> PP a
serialPrefixNetworkRow block f [] = []
serialPrefixNetworkRow block f as = (serialPrefixNetwork block f a0s) ++ serialPrefixNetworkRow block f a1s 
	where
	(a0s,a1s) = splitAt block as
	
serialPrefixNetworkTree :: Int -> PP a
serialPrefixNetworkTree block f [] = []
serialPrefixNetworkTree block f as = aOuts
	where
	a0s = serialPrefixNetworkRow block f as
	aOuts = if (block*block) < (length as)
			then serialPrefixNetwork (block*block) f a0s
			else a0s

rootCalc :: Int->Int->Int->Int
rootCalc i k l = root
	where
	root = if i*k > l
		   then i
		   else rootCalc (i*k) k l

bKungG :: Int -> PP a
--bKungG k f as | length as <= k = undefined
bKungG k f as = [as!!(root-1)]
	where
	root = rootCalc k k (length as)
	ys = serialPrefixNetworkTree k f as-}

--testA6xx = simulate (bKung (mkFan opCount)) (replicate 8 0)

{-putInList :: [a] -> [Int] -> [a] -> [a]
putInList [] [] as = as
putInList (e:els) (i:is) as = out
	where
	(ls,rs) = splitAt (i) as
	newLs = (init ls) ++ [e]
	out = if null els
		  then newLs ++ rs
		  else putInList els is (newLs ++ rs)-}
{-ifRoot :: Int -> Int -> Int
ifRoot num base = out
	where
	out = if num - (base*base)  <= 0
		  then num - (base*base)
		  else ifRoot num (base*base)-}
---- working bKung
{-fanOfOperator :: Int -> PP a
fanOfOperator i f as = result
	where
	op1 = head as
	ops = tail as
	(op2,rops) = if (length ops) == 2
				 then (ops,[])
				 else splitAt (2) ops
	outs = f[op1,last op2]
	result = if null rops
			 then (init op2) ++ [last outs]
			 else (init op2) ++ [last outs] ++ (fanOfOperator (i+1) f (op1:rops))

prefixNetwork :: Int -> PP a
prefixNetwork n f as = cs
	where
	(ops,bs) = splitAt (n*2) as
	(op1,ops2) = splitAt n ops
	op2 = if (length ops2 > 2)
		  then prefixNetwork 2 f ops2
		  else ops2
	outs = fanOfOperator 1 f ([last op1]++op2)
	results = op1 ++ outs -- (init op2) ++ [last outs]
	cs = if length as <= n*2
		 then results ++ bs
		 else prefixNetwork (n*2) f (results ++ bs)-}
		 
		 
		 
		 
		 
		 
-------------------- a8
{-serialPrefixOperator :: Int -> PP a
serialPrefixOperator block f as = outs
	where
	elts = [i*(length as `div` block) | i<-[1..block]]
	ops = [as!!(ind-1) | ind <- elts]
	results = ser f (ops)
	outs = putInList results elts as-}
serialPrefixNetworkTree :: Int -> PP a
serialPrefixNetworkTree k f as = out
	where
	root = serialrootCalc 1 k (length as)
	(ls,rs) = splitAt root as
	xs = serialPrefixNetwork root k f ls
	out = if (serialrootCalc 1 k (length rs)) == 1
		  then xs
		  else xs ++ serialPrefixNetworkTree k f rs	
		  
{-fanPrefixNetworkRow :: Int -> Int -> PP a
fanPrefixNetworkRow root block f as = out
	where
	(notNeeded,needed) = splitAt (root`div`block -1) as
	toOperate = init needed
	splits = if root == block
			 then chop (block) toOperate
			 else chop (root`div`block) toOperate
	fanOps = [fanPrefixOperator block f i | i<-splits]
	out = notNeeded ++ joinLists(fanOps) ++ [last needed]-}
	
	fanPrefixNetworkTree :: Int -> PP a
fanPrefixNetworkTree block f as = xs
	where
	root = fanRootCalc 1 block (length as)
	(ls,rs) = splitAt root as
	xs = fanPrefixNetwork (block*block) block f ls
	out = if null rs
		  then xs
		  else fanPrefixNetwork block block f (drop(block-1) xs ++ rs)
		  
		  
{-fanPrefixNetwork :: Int -> Int -> PP a
fanPrefixNetwork root block f as = out
	where
	result = fanPrefixNetworkRow root block f as
	out = if root == block
		  then result
		  else fanPrefixNetwork (root`div`block) block f result-}